The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^2, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

sum#1(Nil) → 0
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0) → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0, x2) → 0
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0, x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0) → 0
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

S is empty.
Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Innermost TRS:
Rules:
sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Types:
sum#1 :: Nil:Cons → 0':S
Nil :: Nil:Cons
0' :: 0':S
Cons :: 0':S → Nil:Cons → Nil:Cons
plus#2 :: 0':S → 0':S → 0':S
map#2 :: Nil:Cons → Nil:Cons
mult#2 :: 0':S → 0':S → 0':S
unfoldr#2 :: 0':S → Nil:Cons
S :: 0':S → 0':S
main :: 0':S → 0':S
hole_0':S1_0 :: 0':S
hole_Nil:Cons2_0 :: Nil:Cons
gen_0':S3_0 :: Nat → 0':S
gen_Nil:Cons4_0 :: Nat → Nil:Cons

(5) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
sum#1, plus#2, map#2, mult#2, unfoldr#2

They will be analysed ascendingly in the following order:
plus#2 < sum#1
plus#2 < mult#2
mult#2 < map#2

(6) Obligation:

Innermost TRS:
Rules:
sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Types:
sum#1 :: Nil:Cons → 0':S
Nil :: Nil:Cons
0' :: 0':S
Cons :: 0':S → Nil:Cons → Nil:Cons
plus#2 :: 0':S → 0':S → 0':S
map#2 :: Nil:Cons → Nil:Cons
mult#2 :: 0':S → 0':S → 0':S
unfoldr#2 :: 0':S → Nil:Cons
S :: 0':S → 0':S
main :: 0':S → 0':S
hole_0':S1_0 :: 0':S
hole_Nil:Cons2_0 :: Nil:Cons
gen_0':S3_0 :: Nat → 0':S
gen_Nil:Cons4_0 :: Nat → Nil:Cons

Generator Equations:
gen_0':S3_0(0) ⇔ 0'
gen_0':S3_0(+(x, 1)) ⇔ S(gen_0':S3_0(x))
gen_Nil:Cons4_0(0) ⇔ Nil
gen_Nil:Cons4_0(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons4_0(x))

The following defined symbols remain to be analysed:
plus#2, sum#1, map#2, mult#2, unfoldr#2

They will be analysed ascendingly in the following order:
plus#2 < sum#1
plus#2 < mult#2
mult#2 < map#2

(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
plus#2(gen_0':S3_0(n6_0), gen_0':S3_0(b)) → gen_0':S3_0(+(n6_0, b)), rt ∈ Ω(1 + n6₀)

Induction Base:
plus#2(gen_0':S3_0(0), gen_0':S3_0(b)) →_R^Ω(1)
gen_0':S3_0(b)

Induction Step:
plus#2(gen_0':S3_0(+(n6_0, 1)), gen_0':S3_0(b)) →_R^Ω(1)
S(plus#2(gen_0':S3_0(n6_0), gen_0':S3_0(b))) →_IH
S(gen_0':S3_0(+(b, c7_0)))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(8) Complex Obligation (BEST)

(9) Obligation:

Innermost TRS:
Rules:
sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Types:
sum#1 :: Nil:Cons → 0':S
Nil :: Nil:Cons
0' :: 0':S
Cons :: 0':S → Nil:Cons → Nil:Cons
plus#2 :: 0':S → 0':S → 0':S
map#2 :: Nil:Cons → Nil:Cons
mult#2 :: 0':S → 0':S → 0':S
unfoldr#2 :: 0':S → Nil:Cons
S :: 0':S → 0':S
main :: 0':S → 0':S
hole_0':S1_0 :: 0':S
hole_Nil:Cons2_0 :: Nil:Cons
gen_0':S3_0 :: Nat → 0':S
gen_Nil:Cons4_0 :: Nat → Nil:Cons

Lemmas:
plus#2(gen_0':S3_0(n6_0), gen_0':S3_0(b)) → gen_0':S3_0(+(n6_0, b)), rt ∈ Ω(1 + n6₀)

Generator Equations:
gen_0':S3_0(0) ⇔ 0'
gen_0':S3_0(+(x, 1)) ⇔ S(gen_0':S3_0(x))
gen_Nil:Cons4_0(0) ⇔ Nil
gen_Nil:Cons4_0(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons4_0(x))

The following defined symbols remain to be analysed:
sum#1, map#2, mult#2, unfoldr#2

They will be analysed ascendingly in the following order:
mult#2 < map#2

(10) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
sum#1(gen_Nil:Cons4_0(n731_0)) → gen_0':S3_0(0), rt ∈ Ω(1 + n731₀)

Induction Base:
sum#1(gen_Nil:Cons4_0(0)) →_R^Ω(1)
0'

Induction Step:
sum#1(gen_Nil:Cons4_0(+(n731_0, 1))) →_R^Ω(1)
plus#2(0', sum#1(gen_Nil:Cons4_0(n731_0))) →_IH
plus#2(0', gen_0':S3_0(0)) →_L^Ω(1)
gen_0':S3_0(+(0, 0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(11) Complex Obligation (BEST)

(12) Obligation:

Innermost TRS:
Rules:
sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Types:
sum#1 :: Nil:Cons → 0':S
Nil :: Nil:Cons
0' :: 0':S
Cons :: 0':S → Nil:Cons → Nil:Cons
plus#2 :: 0':S → 0':S → 0':S
map#2 :: Nil:Cons → Nil:Cons
mult#2 :: 0':S → 0':S → 0':S
unfoldr#2 :: 0':S → Nil:Cons
S :: 0':S → 0':S
main :: 0':S → 0':S
hole_0':S1_0 :: 0':S
hole_Nil:Cons2_0 :: Nil:Cons
gen_0':S3_0 :: Nat → 0':S
gen_Nil:Cons4_0 :: Nat → Nil:Cons

Lemmas:
plus#2(gen_0':S3_0(n6_0), gen_0':S3_0(b)) → gen_0':S3_0(+(n6_0, b)), rt ∈ Ω(1 + n6₀)
sum#1(gen_Nil:Cons4_0(n731_0)) → gen_0':S3_0(0), rt ∈ Ω(1 + n731₀)

Generator Equations:
gen_0':S3_0(0) ⇔ 0'
gen_0':S3_0(+(x, 1)) ⇔ S(gen_0':S3_0(x))
gen_Nil:Cons4_0(0) ⇔ Nil
gen_Nil:Cons4_0(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons4_0(x))

The following defined symbols remain to be analysed:
mult#2, map#2, unfoldr#2

They will be analysed ascendingly in the following order:
mult#2 < map#2

(13) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
mult#2(gen_0':S3_0(n1062_0), gen_0':S3_0(b)) → gen_0':S3_0(*(n1062_0, b)), rt ∈ Ω(1 + b·n1062₀ + n1062₀)

Induction Base:
mult#2(gen_0':S3_0(0), gen_0':S3_0(b)) →_R^Ω(1)
0'

Induction Step:
mult#2(gen_0':S3_0(+(n1062_0, 1)), gen_0':S3_0(b)) →_R^Ω(1)
plus#2(gen_0':S3_0(b), mult#2(gen_0':S3_0(n1062_0), gen_0':S3_0(b))) →_IH
plus#2(gen_0':S3_0(b), gen_0':S3_0(*(c1063_0, b))) →_L^{Ω(1 + b)}
gen_0':S3_0(+(b, *(n1062_0, b)))

We have rt ∈ Ω(n²) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n²).

(14) Complex Obligation (BEST)

(15) Obligation:

Innermost TRS:
Rules:
sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Types:
sum#1 :: Nil:Cons → 0':S
Nil :: Nil:Cons
0' :: 0':S
Cons :: 0':S → Nil:Cons → Nil:Cons
plus#2 :: 0':S → 0':S → 0':S
map#2 :: Nil:Cons → Nil:Cons
mult#2 :: 0':S → 0':S → 0':S
unfoldr#2 :: 0':S → Nil:Cons
S :: 0':S → 0':S
main :: 0':S → 0':S
hole_0':S1_0 :: 0':S
hole_Nil:Cons2_0 :: Nil:Cons
gen_0':S3_0 :: Nat → 0':S
gen_Nil:Cons4_0 :: Nat → Nil:Cons

Lemmas:
plus#2(gen_0':S3_0(n6_0), gen_0':S3_0(b)) → gen_0':S3_0(+(n6_0, b)), rt ∈ Ω(1 + n6₀)
sum#1(gen_Nil:Cons4_0(n731_0)) → gen_0':S3_0(0), rt ∈ Ω(1 + n731₀)
mult#2(gen_0':S3_0(n1062_0), gen_0':S3_0(b)) → gen_0':S3_0(*(n1062_0, b)), rt ∈ Ω(1 + b·n1062₀ + n1062₀)

Generator Equations:
gen_0':S3_0(0) ⇔ 0'
gen_0':S3_0(+(x, 1)) ⇔ S(gen_0':S3_0(x))
gen_Nil:Cons4_0(0) ⇔ Nil
gen_Nil:Cons4_0(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons4_0(x))

The following defined symbols remain to be analysed:
map#2, unfoldr#2

(16) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
map#2(gen_Nil:Cons4_0(n2038_0)) → gen_Nil:Cons4_0(n2038_0), rt ∈ Ω(1 + n2038₀)

Induction Base:
map#2(gen_Nil:Cons4_0(0)) →_R^Ω(1)
Nil

Induction Step:
map#2(gen_Nil:Cons4_0(+(n2038_0, 1))) →_R^Ω(1)
Cons(mult#2(0', 0'), map#2(gen_Nil:Cons4_0(n2038_0))) →_L^Ω(1)
Cons(gen_0':S3_0(*(0, 0)), map#2(gen_Nil:Cons4_0(n2038_0))) →_IH
Cons(gen_0':S3_0(0), gen_Nil:Cons4_0(c2039_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(17) Complex Obligation (BEST)

(18) Obligation:

Innermost TRS:
Rules:
sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Types:
sum#1 :: Nil:Cons → 0':S
Nil :: Nil:Cons
0' :: 0':S
Cons :: 0':S → Nil:Cons → Nil:Cons
plus#2 :: 0':S → 0':S → 0':S
map#2 :: Nil:Cons → Nil:Cons
mult#2 :: 0':S → 0':S → 0':S
unfoldr#2 :: 0':S → Nil:Cons
S :: 0':S → 0':S
main :: 0':S → 0':S
hole_0':S1_0 :: 0':S
hole_Nil:Cons2_0 :: Nil:Cons
gen_0':S3_0 :: Nat → 0':S
gen_Nil:Cons4_0 :: Nat → Nil:Cons

Lemmas:
plus#2(gen_0':S3_0(n6_0), gen_0':S3_0(b)) → gen_0':S3_0(+(n6_0, b)), rt ∈ Ω(1 + n6₀)
sum#1(gen_Nil:Cons4_0(n731_0)) → gen_0':S3_0(0), rt ∈ Ω(1 + n731₀)
mult#2(gen_0':S3_0(n1062_0), gen_0':S3_0(b)) → gen_0':S3_0(*(n1062_0, b)), rt ∈ Ω(1 + b·n1062₀ + n1062₀)
map#2(gen_Nil:Cons4_0(n2038_0)) → gen_Nil:Cons4_0(n2038_0), rt ∈ Ω(1 + n2038₀)

Generator Equations:
gen_0':S3_0(0) ⇔ 0'
gen_0':S3_0(+(x, 1)) ⇔ S(gen_0':S3_0(x))
gen_Nil:Cons4_0(0) ⇔ Nil
gen_Nil:Cons4_0(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons4_0(x))

The following defined symbols remain to be analysed:
unfoldr#2

(19) Obligation:

Innermost TRS:
Rules:
sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Types:
sum#1 :: Nil:Cons → 0':S
Nil :: Nil:Cons
0' :: 0':S
Cons :: 0':S → Nil:Cons → Nil:Cons
plus#2 :: 0':S → 0':S → 0':S
map#2 :: Nil:Cons → Nil:Cons
mult#2 :: 0':S → 0':S → 0':S
unfoldr#2 :: 0':S → Nil:Cons
S :: 0':S → 0':S
main :: 0':S → 0':S
hole_0':S1_0 :: 0':S
hole_Nil:Cons2_0 :: Nil:Cons
gen_0':S3_0 :: Nat → 0':S
gen_Nil:Cons4_0 :: Nat → Nil:Cons

Lemmas:
plus#2(gen_0':S3_0(n6_0), gen_0':S3_0(b)) → gen_0':S3_0(+(n6_0, b)), rt ∈ Ω(1 + n6₀)
sum#1(gen_Nil:Cons4_0(n731_0)) → gen_0':S3_0(0), rt ∈ Ω(1 + n731₀)
mult#2(gen_0':S3_0(n1062_0), gen_0':S3_0(b)) → gen_0':S3_0(*(n1062_0, b)), rt ∈ Ω(1 + b·n1062₀ + n1062₀)
map#2(gen_Nil:Cons4_0(n2038_0)) → gen_Nil:Cons4_0(n2038_0), rt ∈ Ω(1 + n2038₀)

Generator Equations:
gen_0':S3_0(0) ⇔ 0'
gen_0':S3_0(+(x, 1)) ⇔ S(gen_0':S3_0(x))
gen_Nil:Cons4_0(0) ⇔ Nil
gen_Nil:Cons4_0(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons4_0(x))

No more defined symbols left to analyse.

(20) Obligation:

Innermost TRS:
Rules:
sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Types:
sum#1 :: Nil:Cons → 0':S
Nil :: Nil:Cons
0' :: 0':S
Cons :: 0':S → Nil:Cons → Nil:Cons
plus#2 :: 0':S → 0':S → 0':S
map#2 :: Nil:Cons → Nil:Cons
mult#2 :: 0':S → 0':S → 0':S
unfoldr#2 :: 0':S → Nil:Cons
S :: 0':S → 0':S
main :: 0':S → 0':S
hole_0':S1_0 :: 0':S
hole_Nil:Cons2_0 :: Nil:Cons
gen_0':S3_0 :: Nat → 0':S
gen_Nil:Cons4_0 :: Nat → Nil:Cons

Lemmas:
plus#2(gen_0':S3_0(n6_0), gen_0':S3_0(b)) → gen_0':S3_0(+(n6_0, b)), rt ∈ Ω(1 + n6₀)
sum#1(gen_Nil:Cons4_0(n731_0)) → gen_0':S3_0(0), rt ∈ Ω(1 + n731₀)
mult#2(gen_0':S3_0(n1062_0), gen_0':S3_0(b)) → gen_0':S3_0(*(n1062_0, b)), rt ∈ Ω(1 + b·n1062₀ + n1062₀)

Generator Equations:
gen_0':S3_0(0) ⇔ 0'
gen_0':S3_0(+(x, 1)) ⇔ S(gen_0':S3_0(x))
gen_Nil:Cons4_0(0) ⇔ Nil
gen_Nil:Cons4_0(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons4_0(x))

No more defined symbols left to analyse.

(21) Obligation:

Innermost TRS:
Rules:
sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Types:
sum#1 :: Nil:Cons → 0':S
Nil :: Nil:Cons
0' :: 0':S
Cons :: 0':S → Nil:Cons → Nil:Cons
plus#2 :: 0':S → 0':S → 0':S
map#2 :: Nil:Cons → Nil:Cons
mult#2 :: 0':S → 0':S → 0':S
unfoldr#2 :: 0':S → Nil:Cons
S :: 0':S → 0':S
main :: 0':S → 0':S
hole_0':S1_0 :: 0':S
hole_Nil:Cons2_0 :: Nil:Cons
gen_0':S3_0 :: Nat → 0':S
gen_Nil:Cons4_0 :: Nat → Nil:Cons

Lemmas:
plus#2(gen_0':S3_0(n6_0), gen_0':S3_0(b)) → gen_0':S3_0(+(n6_0, b)), rt ∈ Ω(1 + n6₀)
sum#1(gen_Nil:Cons4_0(n731_0)) → gen_0':S3_0(0), rt ∈ Ω(1 + n731₀)

Generator Equations:
gen_0':S3_0(0) ⇔ 0'
gen_0':S3_0(+(x, 1)) ⇔ S(gen_0':S3_0(x))
gen_Nil:Cons4_0(0) ⇔ Nil
gen_Nil:Cons4_0(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons4_0(x))

No more defined symbols left to analyse.

(22) Obligation:

Innermost TRS:
Rules:
sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Types:
sum#1 :: Nil:Cons → 0':S
Nil :: Nil:Cons
0' :: 0':S
Cons :: 0':S → Nil:Cons → Nil:Cons
plus#2 :: 0':S → 0':S → 0':S
map#2 :: Nil:Cons → Nil:Cons
mult#2 :: 0':S → 0':S → 0':S
unfoldr#2 :: 0':S → Nil:Cons
S :: 0':S → 0':S
main :: 0':S → 0':S
hole_0':S1_0 :: 0':S
hole_Nil:Cons2_0 :: Nil:Cons
gen_0':S3_0 :: Nat → 0':S
gen_Nil:Cons4_0 :: Nat → Nil:Cons

Lemmas:
plus#2(gen_0':S3_0(n6_0), gen_0':S3_0(b)) → gen_0':S3_0(+(n6_0, b)), rt ∈ Ω(1 + n6₀)

Generator Equations:
gen_0':S3_0(0) ⇔ 0'
gen_0':S3_0(+(x, 1)) ⇔ S(gen_0':S3_0(x))
gen_Nil:Cons4_0(0) ⇔ Nil
gen_Nil:Cons4_0(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons4_0(x))

No more defined symbols left to analyse.